FDL - fincr_wf

fincr_wf_com

Note that is this case, we use a supertype of the
range to prove that 'FIncr' is well formed. Then,
in the prove of wf, we show that 'f' with a restricted
domain lies in the type '

'. Afterwards, we use
the fact that 'f(i)

' for an unrestricted range.
We are duplicating work.

origin